There are two categories of verification methods presently known for verifying digital circuit designs. In one category are simulation methods in which various combinations of inputs are applied to a computer model of the circuit and signals at various places in the circuit are observed. The problem with these verification methods is that for complex circuits there is simply not enough time to apply all possible combinations of inputs. Circuits that are verified using this method have been known to contain errors that are only subsequently discovered.
The other circuit design verification method category comprises formal proofs in which from a description of a circuit it is proved that the circuit behaves in the specified way. It is therefore necessary to prepare a behavioral specification of the circuit and then determine by proofs whether the circuit model satisfies the specified behavioral requirements.
There are several different techniques known in the circuit verification art for modeling digital circuit hardware for verification by formal proof. One such technique uses a register-transfer model in which hardware devices are divided into combinational and sequential device types. Both types of devices are described by functions, with the sequential device functions taking an extra argument representing an internal state when the circuit is clocked. Aspects of the register-transfer model are described in "A Very Simple Model of Sequential Behavior of nMOS", by Gordon, Proc. VLSI International Conference, J. Gray Editor, Academic Press, London and New York, 1981 and "FM8501: A Verified Microprocessor" by Hunt, Jr., Technical Report 47, University of Texas at Austin, December 1985.
A second modeling technique uses state transition models where each circuit device is modeled by a state machine. Connections between the devices are represented by equating some state variables of one device with those of another device. Aspects of the state transition model are described in "Proving the Correctness of Digital Hardware Designs" by Barrow, VLSI Design, July 1984.
In a third modeling technique, hardware devices are specified using predicates that constrain the values present on lines interconnecting the devices. Aspects of the predicate model are described in "Why Higher-Order Logic is a Good Formalism for Specifying and Verifying Hardware" by Gordon, Technical Report, University of Cambridge, Cambridge, U.K., 1985 and "A Temporal Logic for Multilevel Reasoning About Hardware" by Moszkowski, IEEE Computer, February 1985.
A primary disadvantage of the register-transfer and state transition models is their inability to represent as bidirectional an individual line into a circuit device. While the predicate model can represent such lines as bidirectional, it fails to capture all relevant aspects of bidirectionality. This shortcoming of the predicate model is illustrated with respect to a CMOS implementation of an inverter, such an inverter 100 being illustrated in FIG. 1. The letters "i" and "o" are shown to denote the input and the output lines, respectively, of the inverter. In accordance with the predicate model of the inverter, it can be shown to satisfy the specification:
Inverter(i,o){(o.dbd. i) PA1 Inverter(i,o){(i.dbd. o)
where is the "not" operator of predicate logic. Note, however, that since (o.dbd. i){(i.dbd. o), there follows:
which implies that the device will function as an inverter in either of two ways, i.e. with either i or o designated as its input line. It is evident that the actual circuit will not operate as an inverter in both such ways, but only with the line i being the input line. Thus, in the illustrated example, the predicate model provides an erroneous representation of bidirectionality. It would therefore be desirable to provide a digital circuit modeling technique, for use in circuit verification by formal proof, that enables accurate modeling of line bidirectionality.
The above described prior art modeling techniques also fail to provide means for modeling charge sharing. It would therefore be desirable to provide a digital circuit modeling technique for use in circuit verification by formal proof, that enables modeling of charge sharing.
It is therefore a principal object of the present invention to provide a system and method for modeling digital circuitry, for use in circuit design verification by formal proof, that is not subject to the aforementioned problems and disadvantages.